should-forward(es; In; isupdate; f; a)
== (((a  In)) & ((isupdate(In(a)))))  ((((a  In))) & ((loc(f(a)) = loc(a)))) 

latex

---

clarification:

should-forward(es; In; isupdate; f; a)
== (((a  In)) & ((isupdate(In(a)))))
==  ((((a  In))) & ((es-loc(es; (f(a))) = es-loc(es; a)  Id))) 

latex

Up	abstract chain replication
Wellformedness Lemmas	should-forward wf
Definitions	P  Q, X(e), P & Q, b, e  X, A, s = t, Id, f(a), loc(e)
FDL editor aliases	should-forward